es:event_system{i:l}, i,x:Id, T:Type, L:(Knd List). frame-p(es; i; T; x; L)  prop{i:l} 

latex

Definitions	True, T, x. t(x), A, P  Q, A c B, frame-p(es; i; T; x; L), prop{i:l}, t  T, x:A. B(x), es_vartype(es; i; x), es_state(es; i), x(s), es-vartype(es; i; x)
Lemmas	event system wf, Knd wf, es state when wf, es-vartype wf, true wf, squash wf, subtype rel wf, es state wf, es state after wf, false wf, l member wf, es-loc wf, Id wf, alle-at wf